COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	more arithmetic
C00005 00003	minus
C00017 ENDMK
C⊗;
;more arithmetic
(wipe-out)
(get-proofs normal prf ekl sys)
(get-proofs natnum prf ekl sys)
(label simpinfo zero_not_successor) ;add these to simpinfo for now
(label simpinfo zeroleast1)
(label simpinfo successorless)
(label simpinfo successoreq)
(label simpinfo zeroleast3)

(proof lesseq)

;1
(axiom |∀n.¬n=n'|)
(label simpinfo)

;2
(decl lesseq (type: |ground⊗ground→truthval|)
      (syntype: constant) (infixname: |≤|)(bindingpower: 920))

;3
(define lesseq |∀m n.(m ≤ n)=(m=n∨m<n)|)
(label lesseqdef)

;4
(axiom |∀n m.n'≤m'≡n≤m|)
(label successorlesseq) (label successorfacts) (label simpinfo)

;5
(axiom |∀n m k.n≤m∧m≤k⊃n≤k|)
(label trans_lesseq)

;6
(axiom |∀n m k.n<m∧m≤k⊃n<k|)
(label less_lesseq_fact1)

;7
(axiom |∀n.0≤n|)
(label zeroleast)

;8
(axiom |∀n.1≤n'|)
(label oneleastsucc)

;9
(axiom |∀n m.n'<m⊃¬m=0|)
(label zero_non_less_successor)(label simpinfo)
;10

(axiom |∀m n.m'<n⊃m<n|)
(label succ_less_less)
;11
(axiom |∀m n.m'≤n⊃m≤n|)
(label succ_lesseq_lesseq)

;12
(axiom |∀n m.n≤m⊃n≤m'|)
(label lesseq_lesseq_succ)

;13
(axiom |∀n m.m<n'≡m≤n|)
(label less_succ_lesseq)

;14
(axiom |∀m n.m<n=m'≤n|)
(label less_lesseqsucc)

;15
(axiom |∀n m.n≤m∧m≤n⊃n=m|)
(label leq_leq_eq)

;16
(axiom |∀n m.m<n∨m=n∨n<m|)
(label trichotomy)

;minus
(proof minus)

;1. 
(decl minus (type: |ground⊗ground→ground|)(infixname: |-|)
      (syntype: constant) (bindingpower: 940))

;2. 
(define minus |∀m n.m-0=m∧m-(n')=pred(m-n)| inductive_definition)
(label minusdef)

;3.
(axiom |∀n k.natnum(k-n)|)
(label simpinfo)(label minus_sort)

;4.
(axiom |∀n m.n<m⊃0<m-n|)
(label minusfact3)

;5.
(axiom |∀n.0<n⊃pred(n)'=n|)
(label minusfact5)

;6.
(axiom |∀n m.n≤m⊃m'-n=(m-n)'|)
(label successor_minus)

;7.
(axiom |∀n m.n<m⊃m-n=(m-(n'))'|)
(label minusfact10)

;8.
(axiom |∀n m.m<n⊃n-(m')<n|)
(label minusfact11)

;9.
(axiom |∀n.n-n=0|)
(label simpinfo)(label n_less_n)

;10.
(axiom |∀n.0<n⊃n-(pred n)=1|)
(label minus1)

;11.
(axiom |∀n m.m≤n⊃m-n=0|)
(label total_subtraction)

;12.
(axiom |∀n m k.k<n∧m<n-k≡m+k<n|)
(label inequality_law)

;the main facts of arithmetic needed for the pigeon-hole

;13.
(axiom |∀n k m.n≤m∧1≤k⊃n'≤m+k|)
(label add_lesseq)

;14.
(axiom |∀k n m.1≤k∧m+k=n'∧n≤m⊃1=k∧n=m|)
(label add_one)
(save-proofs minus)